1  /-
  2  Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel, Mario Carneiro
  5  
  6  Type of bounded continuous functions taking values in a metric space, with
  7  the uniform distance.
  8   -/
  9  
 10  import analysis.normed_space.basic topology.metric_space.lipschitz
src         └─────────────────────────┘ └─────────────────────────────┘
 11  
 12  noncomputable theory
 13  local attribute [instance] classical.decidable_inhabited classical.prop_decidable
 14  open_locale topological_space
 15  
 16  open set lattice filter metric
 17  
 18  universes u v w
 19  variables {α : Type u} {β : Type v} {γ : Type w}
 20  
 21  /-- A locally uniform limit of continuous functions is continuous -/
 22  lemma continuous_of_locally_uniform_limit_of_continuous [topological_space α] [metric_space β]
 23    {F : ℕ → α → β} {f : α → β}
id                          
src         
typ                         
 24    (L : ∀x:α, ∃s ∈ 𝓝 x, ∀ε>(0:ℝ), ∃n, ∀y∈s, dist (F n y) (f y) ≤ ε)
id                                 └──┘           
src                                     └──┘               
typ                                └──┘           
doc                    
 25    (C : ∀ n, continuous (F n)) : continuous f :=
id              └────────┘        └────────┘ 
src              └────────┘          └────────┘
typ             └────────┘        └────────┘ 
doc              └────────┘          └────────┘
 26  continuous_iff'.2 $ λ x ε ε0, begin
id   └─────────────┘        └┘
src  └─────────────┘
typ  └─────────────┘        └┘
st                                 └─────
 27    rcases L x with ⟨r, rx, hr⟩,
id             
src    └─────┘  └───────────────┘
typ    └─────┘└───────────────┘
doc    └─────┘  └───────────────┘
txt    └─────┘  └───────────────┘
par    └─────┘  └───────────────┘
pid            └───────────────┘
st   ────────────────────────────┘└─
 28    rcases hr (ε/2/2) (half_pos $ half_pos ε0) with ⟨n, hn⟩,
id            └┘                   └──────┘ └┘
src    └─────┘     └─┘          └──────┘  └────────────┘
typ    └─────┘└┘  └─┘          └──────┘└┘└────────────┘
doc    └─────┘      └─┘                    └────────────┘
txt    └─────┘      └─┘                    └────────────┘
par    └─────┘      └─┘                    └────────────┘
pid                └─┘                    └────────────┘
st   ────────────────────────────────────────────────────────┘└─
 29    rcases continuous_iff'.1 (C n) x (ε/2) (half_pos ε0) with ⟨s, sx, hs⟩,
id            └─────────────┘              └──────┘ └┘
src    └─────┘└─────────────┘└─┘   └┘    └─┘ └──────┘  └────────────────┘
typ    └─────┘└─────────────┘└─┘ └┘  └─┘ └──────┘└┘└────────────────┘
doc    └─────┘               └─┘   └┘    └─┘           └────────────────┘
txt    └─────┘               └─┘   └┘    └─┘           └────────────────┘
par    └─────┘               └─┘   └┘    └─┘           └────────────────┘
pid                         └─┘   └┘    └─┘           └────────────────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
 30    refine ⟨_, (𝓝 x).inter_sets rx sx, _⟩,
id                               └┘ └┘
src    └─────┘ └─┘  └───────────┘    └──┘
typ    └─────┘ └─┘ └───────────┘└┘└┘└──┘
doc    └─────┘ └─┘  └───────────┘    └──┘
txt    └─────┘ └─┘   └───────────┘    └──┘
par    └─────┘ └─┘   └───────────┘    └──┘
pid           └─┘   └───────────┘    └──┘
st   ──────────────────────────────────────┘└─
 31    rintro y ⟨yr, ys⟩,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid          └─────────┘
st   ──────────────────┘└─
 32    calc dist (f y) (f x)
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ────────────────────────
 33          ≤ dist (F n y) (F n x) + (dist (F n y) (f y) + dist (F n x) (f x)) : dist_triangle4_left _ _ _ _
id                                                         └──┘              └─────────────────┘
src                                                         └──┘                  └─────────────────┘
typ                                                        └──┘              └─────────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────
 34      ... < ε/2 + (ε/2/2 + ε/2/2) :
id                 
src                
typ                
st   ──────────────────────────────────
 35        add_lt_add_of_lt_of_le (hs _ ys) (add_le_add (hn _ yr) (hn _ (mem_of_nhds rx)))
id         └────────────────────┘  └┘   └┘   └────────┘       └┘   └┘    └─────────┘ └┘
src        └────────────────────┘            └────────┘                  └─────────┘
typ        └────────────────────┘  └┘   └┘   └────────┘       └┘   └┘    └─────────┘ └┘
st   ──────────────────────────────────────────────────────────────────────────────────────
 36      ... = ε : by rw [add_halves, add_halves]
id                       └────────┘  └────────┘
src                   └──┘└────────┘└┘└────────┘└┘
typ                  └──┘└────────┘└┘└────────┘└┘
doc                   └──┘          └┘          └┘
txt                   └──┘          └┘          └┘
par                   └──┘          └┘          └┘
pid                     └┘          └┘          
st   ───────────────┘└─────────────┘└──────────┘
 37  end
st   └─┘
 38  
 39  /-- A uniform limit of continuous functions is continuous -/
 40  lemma continuous_of_uniform_limit_of_continuous [topological_space α] {β : Type v} [metric_space β]
id                                                    └───────────────┘                 └──────────┘ 
src                                                   └───────────────┘                  └──────────┘
typ                                                   └───────────────┘                 └──────────┘ 
doc                                                   └───────────────┘                  └──────────┘
 41    {F : ℕ → α → β} {f : α → β} (L : ∀ε>(0:ℝ), ∃N, ∀y, dist (F N y) (f y) ≤ ε) :
id                                             └──┘           
src                                                   └──┘               
typ                                            └──┘           
 42    (∀ n, continuous (F n)) → continuous f :=
id          └────────┘        └────────┘ 
src          └────────┘          └────────┘
typ         └────────┘        └────────┘ 
doc          └────────┘          └────────┘
 43  continuous_of_locally_uniform_limit_of_continuous $ λx,
id   └───────────────────────────────────────────────┘    
src  └───────────────────────────────────────────────┘
typ  └───────────────────────────────────────────────┘    
doc  └───────────────────────────────────────────────┘
 44    ⟨univ, by simpa [filter.univ_mem_sets] using L⟩
id      └──┘            └──────────────────┘        
src     └──┘     └─────┘└──────────────────┘└──────┘
typ     └──┘     └─────┘└──────────────────┘└──────┘
doc              └─────┘                    └──────┘
txt              └─────┘                    └──────┘
par              └─────┘                    └──────┘
pid                                       └────┘
st              └───────────────────────────────────┘
 45  
 46  /-- The type of bounded continuous functions from a topological space to a metric space -/
 47  def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] : Type (max u v) :=
id                                                              └───────────────┘    └──────────┘ 
src                                                             └───────────────┘     └──────────┘
typ                                                             └───────────────┘    └──────────┘ 
doc                                                             └───────────────┘     └──────────┘
 48  {f : α → β // continuous f ∧ ∃C, ∀x y:α, dist (f x) (f y) ≤ C}
id             └────────┘           └──┘          
src               └────────┘              └──┘             
typ            └────────┘           └──┘          
doc                └────────┘
 49  
 50  local infixr ` →ᵇ `:25 := bounded_continuous_function
id                             └─────────────────────────┘
src                            └─────────────────────────┘
typ                            └─────────────────────────┘
doc                            └─────────────────────────┘
 51  
 52  namespace bounded_continuous_function
 53  section basics
 54  variables [topological_space α] [metric_space β] [metric_space γ]
id              └───────────────┘    └──────────┘     └──────────┘
src             └───────────────┘     └──────────┘     └──────────┘
typ             └───────────────┘    └──────────┘     └──────────┘
doc             └───────────────┘     └──────────┘     └──────────┘
 55  variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id                      └┘                 
src                     └┘                 
typ                     └┘                 
doc                     └┘
 56  
 57  instance : has_coe_to_fun (α →ᵇ β) :=  ⟨_, subtype.val⟩
id              └────────────┘   └┘           └─────────┘
src             └────────────┘    └┘            └─────────┘
typ             └────────────┘   └┘           └─────────┘
doc                               └┘
 58  
 59  lemma bounded_range : bounded (range f) :=
id                         └─────┘  └───┘ 
src                        └─────┘  └───┘
typ                        └─────┘  └───┘ 
doc                        └─────┘  └───┘
 60  bounded_range_iff.2 f.2.2
id   └───────────────┘   
src  └───────────────┘    
typ  └───────────────┘   
doc  └───────────────┘
 61  
 62  /-- If a function is continuous on a compact space, it is automatically bounded,
 63  and therefore gives rise to an element of the type of bounded continuous functions -/
 64  def mk_of_compact [compact_space α] (f : α → β) (hf : continuous f) : α →ᵇ β :=
id                      └───────────┘                   └────────┘      └┘ 
src                     └───────────┘                      └────────┘        └┘
typ                     └───────────┘                   └────────┘      └┘ 
doc                     └───────────┘                      └────────┘        └┘
 65  ⟨f, hf, bounded_range_iff.1 $ bounded_of_compact $ compact_range hf⟩
id      └┘  └───────────────┘    └────────────────┘   └───────────┘ └┘
src          └───────────────┘    └────────────────┘   └───────────┘
typ     └┘  └───────────────┘    └────────────────┘   └───────────┘ └┘
doc          └───────────────┘     └────────────────┘
 66  
 67  /-- If a function is bounded on a discrete space, it is automatically continuous,
 68  and therefore gives rise to an element of the type of bounded continuous functions -/
 69  def mk_of_discrete [discrete_topology α] (f : α → β) (hf : ∃C, ∀x y, dist (f x) (f y) ≤ C) :
id                       └───────────────┘                        └──┘          
src                      └───────────────┘                              └──┘             
typ                      └───────────────┘                        └──┘          
doc                      └───────────────┘
 70    α →ᵇ β :=
id      └┘ 
src      └┘
typ     └┘ 
doc      └┘
 71  ⟨f, continuous_of_discrete_topology, hf⟩
id      └─────────────────────────────┘  └┘
src      └─────────────────────────────┘
typ     └─────────────────────────────┘  └┘
 72  
 73  /-- The uniform distance between two bounded continuous functions -/
 74  instance : has_dist (α →ᵇ β) :=
id              └──────┘   └┘ 
src             └──────┘    └┘
typ             └──────┘   └┘ 
doc             └──────┘    └┘
 75  ⟨λf g, Inf {C | C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C}⟩
id        └─┘                 └──┘          
src         └─┘                    └──┘             
typ       └─┘                 └──┘          
doc         └─┘
 76  
 77  lemma dist_eq : dist f g = Inf {C | C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C} := rfl
id                   └──┘    └─┘                 └──┘               └─┘
src                  └──┘      └─┘                    └──┘                    └─┘
typ                  └──┘    └─┘                 └──┘               └─┘
doc                             └─┘
 78  
 79  lemma dist_set_exists : ∃ C, C ≥ 0 ∧ ∀ x : α, dist (f x) (g x) ≤ C :=
id                                          └──┘          
src                                            └──┘             
typ                                         └──┘          
 80  begin
st   └─────
 81    refine if h : nonempty α then _ else ⟨0, le_refl _, λ x, h.elim ⟨x⟩⟩,
id            └┘     └──────┘                 └─────┘          └───┘
src    └─────┘└┘└───┘└──────┘ └───────────┘└─┘└─────┘└──┘ └──┘ └───┘  └┘
typ    └─────┘└┘└───┘└──────┘└───────────┘└─┘└─────┘└──┘ └──┘ └───┘  └┘
doc    └─────┘  └───┘         └───────────┘ └─┘       └──┘ └──┘        └┘
txt    └─────┘  └───┘         └───────────┘ └─┘       └──┘ └──┘        └┘
par    └─────┘  └───┘         └───────────┘ └─┘       └──┘ └──┘        └┘
pid            └───┘         └───────────┘ └─┘       └──┘ └──┘        └┘
st   ─────────────────────────────────────────────────────────────────────┘└─
 82    cases h with x,
id           
src    └────┘ └─────┘
typ    └────┘└─────┘
doc    └────┘ └─────┘
txt    └────┘ └─────┘
par    └────┘ └─────┘
pid          └─────┘
st   ───────────────┘└─
 83    rcases f.2 with ⟨_, Cf, hCf⟩, /- hCf : ∀ (x y : α), dist (f.val x) (f.val y) ≤ Cf -/
id            
src    └─────┘ └──────────────────┘
typ    └─────┘└──────────────────┘
doc    └─────┘ └──────────────────┘
txt    └─────┘ └──────────────────┘
par    └─────┘ └──────────────────┘
pid           └──────────────────┘
st   ─────────────────────────────┘└────────────────────────────────────────────────────────
 84    rcases g.2 with ⟨_, Cg, hCg⟩, /- hCg : ∀ (x y : α), dist (g.val x) (g.val y) ≤ Cg -/
id            
src    └─────┘ └──────────────────┘
typ    └─────┘└──────────────────┘
doc    └─────┘ └──────────────────┘
txt    └─────┘ └──────────────────┘
par    └─────┘ └──────────────────┘
pid           └──────────────────┘
st   ─────────────────────────────┘└────────────────────────────────────────────────────────
 85    let C := max 0 (dist (f x) (g x) + (Cf + Cg)),
id              └─┘    └──┘            └┘   └┘
src    └───────┘└─┘└─┘ └──┘   └┘   └┘      └┘
typ    └───────┘└─┘└─┘ └──┘  └┘ └┘ └┘ └┘└┘
doc    └───────┘   └─┘        └┘   └┘       └┘
txt    └───────┘   └─┘        └┘   └┘       └┘
par    └───────┘   └─┘        └┘   └┘       └┘
pid    └───┘└─┘   └─┘        └┘   └┘       └┘
st   ──────────────────────────────────────────────┘└─
 86    exact ⟨C, le_max_left _ _, λ y, calc
id               └─────────┘
src    └────┘  └┘└─────────┘└────┘ └──┘    
typ    └────┘  └┘└─────────┘└────┘ └──┘    
doc    └────┘  └┘           └────┘ └──┘    
txt    └────┘  └┘           └────┘ └──┘    
par    └────┘  └┘           └────┘ └──┘    
pid           └┘           └────┘ └──┘    
st   ───────────────────────────────────────
 87      dist (f y) (g y) ≤ dist (f x) (g x) + (dist (f x) (f y) + dist (g x) (g y)) : dist_triangle4_left _ _ _ _
id                                                                └──┘              └─────────────────┘
src  ───┘       └┘   └┘        └┘   └┘         └┘   └┘ └──┘   └┘   └───┘└─────────────────┘└────────
typ  ───┘       └┘   └┘        └┘   └┘         └┘  └┘ └──┘  └┘  └───┘└─────────────────┘└────────
doc  ───┘       └┘   └┘        └┘   └┘         └┘   └┘        └┘   └───┘                   └────────
txt  ───┘       └┘   └┘        └┘   └┘         └┘   └┘        └┘   └───┘                   └────────
par  ───┘       └┘   └┘        └┘   └┘         └┘   └┘        └┘   └───┘                   └────────
pid  ───┘       └┘   └┘        └┘   └┘         └┘   └┘        └┘   └───┘                   └────────
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
 88                  ... ≤ dist (f x) (g x) + (Cf + Cg) : add_le_add_left (add_le_add (hCf _ _) (hCg _ _)) _
id                                             └┘   └┘    └─────────────┘  └────────┘  └─┘       └─┘
src  ───────────────────┘        └┘   └┘       └──┘└─────────────┘ └────────┘    └────┘    └────────
typ  ───────────────────┘        └┘   └┘  └┘ └┘└──┘└─────────────┘ └────────┘ └─┘└────┘ └─┘└────────
doc  ───────────────────┘        └┘   └┘       └──┘                              └────┘    └────────
txt  ───────────────────┘        └┘   └┘       └──┘                              └────┘    └────────
par  ───────────────────┘        └┘   └┘       └──┘                              └────┘    └────────
pid  ───────────────────┘        └┘   └┘       └──┘                              └────┘    └────────
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────
 89                  ... ≤ C : le_max_right _ _⟩
id                            └──────────┘
src  ───────────────────┘  └─┘└──────────┘└────┘
typ  ───────────────────┘ └─┘└──────────┘└────┘
doc  ───────────────────┘  └─┘            └────┘
txt  ───────────────────┘  └─┘            └────┘
par  ───────────────────┘  └─┘            └────┘
pid  ───────────────────┘  └─┘            └───┘
st   ───────────────────────────────────────────┘
 90  end
st   └─┘
 91  
 92  /-- The pointwise distance is controlled by the distance between functions, by definition -/
 93  lemma dist_coe_le_dist (x : α) : dist (f x) (g x) ≤ dist f g :=
id                                   └──┘          └──┘  
src                                   └──┘              └──┘
typ                                  └──┘          └──┘  
 94  le_cInf dist_set_exists $ λb hb, hb.2 x
id   └─────┘ └─────────────┘     └┘  └┘  
src  └─────┘ └─────────────┘            
typ  └─────┘ └─────────────┘     └┘  └┘  
 95  
 96  @[ext] lemma ext (H : ∀x, f x = g x) : f = g :=
id                                      
src                                          
typ                                     
doc    └─┘
 97  subtype.eq $ by ext; apply H
id   └────────┘
src  └────────┘      └─┘  └────┘ 
typ  └────────┘      └─┘  └────┘ 
doc                  └─┘  └────┘ 
txt                  └─┘  └────┘ 
par                  └─┘  └────┘ 
pid                             
st                  └─────────────
 98  
src  
typ  
doc  
txt  
par  
pid  
st   
 99  /- This lemma will be needed in the proof of the metric space instance, but it will become
src  ───────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────
100  useless afterwards as it will be superceded by the general result that the distance is nonnegative
src  ───────────────────────────────────────────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
101  is metric spaces. -/
src  ────────────────────┘
typ  ────────────────────┘
doc  ────────────────────┘
txt  ────────────────────┘
par  ────────────────────┘
pid  ────────────────────┘
st   ────────────────────┘
102  private lemma dist_nonneg' : 0 ≤ dist f g :=
id                                   └──┘  
src                                  └──┘
typ                                  └──┘  
103  le_cInf dist_set_exists (λ C, and.left)
id   └─────┘ └─────────────┘      └──────┘
src  └─────┘ └─────────────┘       └──────┘
typ  └─────┘ └─────────────┘      └──────┘
104  
105  /-- The distance between two functions is controlled by the supremum of the pointwise distances -/
106  lemma dist_le (C0 : (0 : ℝ) ≤ C) : dist f g ≤ C ↔ ∀x:α, dist (f x) (g x) ≤ C :=
id                                   └──┘           └──┘          
src                                   └──┘               └──┘             
typ                                  └──┘           └──┘          
107  ⟨λ h x, le_trans (dist_coe_le_dist x) h, λ H, cInf_le ⟨0, λ C, and.left⟩ ⟨C0, H⟩⟩
id         └──────┘  └──────────────┘         └─────┘         └──────┘   └┘  
src          └──────┘  └──────────────┘            └─────┘          └──────┘
typ        └──────┘  └──────────────┘         └─────┘         └──────┘   └┘  
doc                    └──────────────┘
108  
109  /-- On an empty space, bounded continuous functions are at distance 0 -/
110  lemma dist_zero_of_empty (e : ¬ nonempty α) : dist f g = 0 :=
id                                  └──────┘     └──┘   
src                                 └──────┘      └──┘     
typ                                 └──────┘     └──┘   
111  le_antisymm ((dist_le (le_refl _)).2 $ λ x, e.elim ⟨x⟩) dist_nonneg'
id   └─────────┘   └─────┘  └─────┘            └───┘     └──────────┘
src  └─────────┘   └─────┘  └─────┘              └───┘      └──────────┘
typ  └─────────┘   └─────┘  └─────┘            └───┘     └──────────┘
doc                └─────┘
112  
113  /-- The type of bounded continuous functions, with the uniform distance, is a metric space. -/
114  instance : metric_space (α →ᵇ β) :=
id              └──────────┘   └┘ 
src             └──────────┘    └┘
typ             └──────────┘   └┘ 
doc             └──────────┘    └┘
115  { dist_self := λ f, le_antisymm ((dist_le (le_refl _)).2 $ λ x, by simp) dist_nonneg',
id                     └─────────┘   └─────┘  └─────┘                     └──────────┘
src                     └─────────┘   └─────┘  └─────┘                └──┘  └──────────┘
typ                    └─────────┘   └─────┘  └─────┘               └──┘  └──────────┘
doc                                    └─────┘                          └──┘
txt                                                                     └──┘
par                                                                     └──┘
st                                                                     └───┘
116    eq_of_dist_eq_zero := λ f g hfg, by ext x; exact
id                               └─┘
src                                        └───┘  └─────
typ                              └─┘     └───┘  └─────
doc                                        └───┘  └─────
txt                                        └───┘  └─────
par                                        └───┘  └─────
pid                                           └┘       
st                                        └─────────────
117      eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg),
id       └────────────────┘  └─────────┘  └─┘  └──────────────┘    └─────────┘
src  ───┘└────────────────┘ └─────────┘    └──────────────┘└──┘└─────────┘
typ  ───┘└────────────────┘ └─────────┘ └─┘└──────────────┘└──┘└─────────┘
doc  ───┘                                   └──────────────┘└──┘           
txt  ───┘                                                   └──┘           
par  ───┘                                                   └──┘           
pid  ───┘                                                   └──┘           
st   ──────────────────────────────────────────────────────────────────────────┘
118    dist_comm := λ f g, by simp [dist_eq, dist_comm],
id                                └─────┘  └───────┘
src                           └────┘└─────┘└┘└───────┘
typ                         └────┘└─────┘└┘└───────┘
doc                           └────┘       └┘         
txt                           └────┘       └┘         
par                           └────┘       └┘         
pid                                      └┘         
st                           └────────────────────────┘
119    dist_triangle := λ f g h,
id                          
typ                         
120      (dist_le (add_nonneg dist_nonneg' dist_nonneg')).2 $ λ x,
id        └─────┘  └────────┘ └──────────┘ └──────────┘        
src       └─────┘  └────────┘ └──────────┘ └──────────┘  
typ       └─────┘  └────────┘ └──────────┘ └──────────┘        
doc       └─────┘
121        le_trans (dist_triangle _ _ _) (add_le_add (dist_coe_le_dist _) (dist_coe_le_dist _)) }
id         └──────┘  └───────────┘         └────────┘  └──────────────┘     └──────────────┘
src        └──────┘  └───────────┘         └────────┘  └──────────────┘     └──────────────┘
typ        └──────┘  └───────────┘         └────────┘  └──────────────┘     └──────────────┘
doc                                                    └──────────────┘     └──────────────┘
122  
123  def const (b : β) : α →ᵇ β := ⟨λx, b, continuous_const, 0, by simp [le_refl]⟩
id                       └┘           └──────────────┘              └─────┘
src                        └┘              └──────────────┘        └────┘└─────┘
typ                      └┘           └──────────────┘        └────┘└─────┘
doc                        └┘                                      └────┘       
txt                                                                └────┘       
par                                                                └────┘       
pid                                                                           
st                                                                └─────────────┘
124  
125  /-- If the target space is inhabited, so is the space of bounded continuous functions -/
126  instance [inhabited β] : inhabited (α →ᵇ β) := ⟨const (default β)⟩
id             └───────┘     └───────┘   └┘       └───┘  └─────┘ 
src            └───────┘      └───────┘    └┘        └───┘  └─────┘
typ            └───────┘     └───────┘   └┘       └───┘  └─────┘ 
doc                                        └┘
127  
128  /-- The evaluation map is continuous, as a joint function of `u` and `x` -/
129  theorem continuous_eval : continuous (λ p : (α →ᵇ β) × α, p.1 p.2) :=
id                             └────────┘          └┘        
src                            └────────┘           └┘            
typ                            └────────┘          └┘        
doc                            └────────┘           └┘
130  continuous_iff'.2 $ λ ⟨f, x⟩ ε ε0,
id   └─────────────┘           └┘
src  └─────────────┘
typ  └─────────────┘           └┘
131  /- use the continuity of `f` to find a neighborhood of `x` where it varies at most by ε/2 -/
132  let ⟨s, sx, Hs⟩ := continuous_iff'.1 f.2.1 x (ε/2) (half_pos ε0) in
id   └─┘    └┘  └┘     └─────────────┘             └──────┘ └┘
src                     └─────────────┘              └──────┘
typ  └─┘    └┘  └┘     └─────────────┘             └──────┘ └┘
133  /- s : set α, sx : s ∈ 𝓝 x, Hs : ∀ (b : α), b ∈ s → dist (f.val b) (f.val x) < ε / 2 -/
134  ⟨set.prod (ball f (ε/2)) s, prod_mem_nhds_sets (ball_mem_nhds _ (half_pos ε0)) sx,
id    └──────┘  └──┘           └────────────────┘  └───────────┘    └──────┘ └┘
src   └──────┘  └──┘            └────────────────┘  └───────────┘    └──────┘
typ   └──────┘  └──┘           └────────────────┘  └───────────┘    └──────┘ └┘
doc   └──────┘  └──┘
135  λ ⟨g, y⟩ ⟨hg, hy⟩, calc dist (g y) (f x)
id         └┘  └┘        └──┘
src                          └──┘
typ        └┘  └┘        └──┘
136        ≤ dist (g y) (f y) + dist (f y) (f x) : dist_triangle _ _ _
id           └──┘              └──┘               └───────────┘
src          └──┘              └──┘               └───────────┘
typ          └──┘              └──┘               └───────────┘
137    ... < ε/2 + ε/2 : add_lt_add (lt_of_le_of_lt (dist_coe_le_dist _) hg) (Hs _ hy)
id                  └────────┘  └────────────┘  └──────────────┘
src                   └────────┘  └────────────┘  └──────────────┘
typ                 └────────┘  └────────────┘  └──────────────┘
doc                                                  └──────────────┘
138    ... = ε : add_halves _⟩
id              └────────┘
src              └────────┘
typ             └────────┘
139  
140  /-- In particular, when `x` is fixed, `f → f x` is continuous -/
141  theorem continuous_evalx {x : α} : continuous (λ f : α →ᵇ β, f x) :=
id                                     └────────┘         └┘    
src                                     └────────┘          └┘
typ                                    └────────┘         └┘    
doc                                     └────────┘          └┘
142  continuous_eval.comp (continuous_id.prod_mk continuous_const)
id   └─────────────┘└───┘  └───────────┘└──────┘ └──────────────┘
src  └─────────────┘└───┘  └───────────┘└──────┘ └──────────────┘
typ  └─────────────┘└───┘  └───────────┘└──────┘ └──────────────┘
doc  └─────────────┘
143  
144  /-- When `f` is fixed, `x → f x` is also continuous, by definition -/
145  theorem continuous_evalf {f : α →ᵇ β} : continuous f := f.2.1
id                                  └┘     └────────┘      
src                                  └┘      └────────┘        
typ                                 └┘     └────────┘      
doc                                  └┘      └────────┘
146  
147  /-- Bounded continuous functions taking values in a complete space form a complete space. -/
148  instance [complete_space β] : complete_space (α →ᵇ β) :=
id             └────────────┘     └────────────┘   └┘ 
src            └────────────┘      └────────────┘    └┘
typ            └────────────┘     └────────────┘   └┘ 
doc            └────────────┘      └────────────┘    └┘
149  complete_of_cauchy_seq_tendsto $ λ (f : ℕ → α →ᵇ β) (hf : cauchy_seq f),
id   └────────────────────────────┘             └┘         └────────┘ 
src  └────────────────────────────┘               └┘          └────────┘
typ  └────────────────────────────┘             └┘         └────────┘ 
doc                                                └┘          └────────┘
150  begin
st   └─────
151    /- We have to show that `f n` converges to a bounded continuous function.
st   ────────────────────────────────────────────────────────────────────────────
152    For this, we prove pointwise convergence to define the limit, then check
st   ───────────────────────────────────────────────────────────────────────────
153    it is a continuous bounded function, and then check the norm convergence. -/
st   ───────────────────────────────────────────────────────────────────────────────
154    rcases cauchy_seq_iff_le_tendsto_0.1 hf with ⟨b, b0, b_bound, b_lim⟩,
id            └─────────────────────────┘   └┘
src    └─────┘└─────────────────────────┘└─┘  └───────────────────────────┘
typ    └─────┘└─────────────────────────┘└─┘└┘└───────────────────────────┘
doc    └─────┘└─────────────────────────┘└─┘  └───────────────────────────┘
txt    └─────┘                           └─┘  └───────────────────────────┘
par    └─────┘                           └─┘  └───────────────────────────┘
pid                                     └─┘  └───────────────────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
155    have f_bdd := λx n m N hn hm, le_trans (dist_coe_le_dist x) (b_bound n m N hn hm),
id                                   └──────┘  └──────────────┘     └─────┘
src    └────────────┘ └─────────────┘└──────┘ └──────────────┘ └┘               
typ    └────────────┘ └─────────────┘└──────┘ └──────────────┘ └┘ └─────┘       
doc    └────────────┘ └─────────────┘         └──────────────┘ └┘               
txt    └────────────┘ └─────────────┘                          └┘               
par    └────────────┘ └─────────────┘                          └┘               
pid    └────────┘└─┘ └─────────────┘                          └┘               
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
156    have fx_cau : ∀x, cauchy_seq (λn, f n x) :=
id                       └────────┘      
src    └────────────┘  └────────┘  └─┘   └────
typ    └────────────┘  └────────┘  └─┘  └────
doc    └────────────┘  └────────┘  └─┘   └────
txt    └────────────┘              └─┘   └────
par    └────────────┘              └─┘   └────
pid    └─────────┘└─┘              └─┘   └───
st   ──────────────────────────────────────────────
157      λx, cauchy_seq_iff_le_tendsto_0.2 ⟨b, b0, f_bdd x, b_lim⟩,
id           └─────────────────────────┘      └┘  └───┘    └───┘
src  ───┘ └─┘└─────────────────────────┘└─┘  └┘  └┘      └┘     
typ  ───┘ └─┘└─────────────────────────┘└─┘ └┘└┘└┘└───┘ └┘└───┘
doc  ───┘ └─┘└─────────────────────────┘└─┘  └┘  └┘      └┘     
txt  ───┘ └─┘                           └─┘  └┘  └┘      └┘     
par  ───┘ └─┘                           └─┘  └┘  └┘      └┘     
pid  ───┘ └─┘                           └─┘  └┘  └┘      └┘     
st   ────────────────────────────────────────────────────────────┘└─
158    choose F hF using λx, cauchy_seq_tendsto_of_complete (fx_cau x),
id                           └────────────────────────────┘  └────┘
src    └────────────────┘ └─┘└────────────────────────────┘        
typ    └────────────────┘ └─┘└────────────────────────────┘ └────┘ 
doc    └────────────────┘ └─┘└────────────────────────────┘        
txt    └────────────────┘ └─┘                                      
par    └────────────────┘ └─┘                                      
pid          └┘└─┘└─────┘ └─┘                                      
st   ────────────────────────────────────────────────────────────────┘└─
159    /- F : α → β,  hF : ∀ (x : α), tendsto (λ (n : ℕ), f n x) at_top (𝓝 (F x))
st   ─────────────────────────────────────────────────────────────────────────────
160    `F` is the desired limit function. Check that it is uniformly approximated by `f N` -/
st   ─────────────────────────────────────────────────────────────────────────────────────────
161    have fF_bdd : ∀x N, dist (f N x) (F x) ≤ b N :=
id                         └──┘              
src    └────────────┘ └─┘ └──┘    └┘   └┘  └───
typ    └────────────┘ └─┘ └──┘   └┘  └┘ └───
doc    └────────────┘ └─┘         └┘   └┘   └───
txt    └────────────┘ └─┘         └┘   └┘   └───
par    └────────────┘ └─┘         └┘   └┘   └───
pid    └─────────┘└─┘ └─┘         └┘   └┘   └───
st   ──────────────────────────────────────────────────
162      λ x N, le_of_tendsto (by simp)
id              └───────────┘
src  ───┘ └────┘└───────────┘   └──┘└─
typ  ───┘ └────┘└───────────┘   └──┘└─
doc  ───┘ └────┘                └──┘└─
txt  ───┘ └────┘                └──┘└─
par  ───┘ └────┘                └──┘└─
pid  ───┘ └────┘                └──────
st   ───────────────────────────┘└───┘└─
163        (tendsto_dist tendsto_const_nhds (hF x))
id          └──────────┘ └────────────────┘  └┘
src  ─────┘ └──────────┘└────────────────┘    └──
typ  ─────┘ └──────────┘└────────────────┘ └┘ └──
doc  ─────┘                                   └──
txt  ─────┘                                   └──
par  ─────┘                                   └──
pid  ─────┘                                   └──
st   ───────────────────────────────────────────────
164        (filter.mem_at_top_sets.2 ⟨N, λn hn, f_bdd x N n N (le_refl N) hn⟩),
id          └────────────────────┘              └───┘          └─────┘
src  ─────┘ └────────────────────┘└─┘  └┘ └────┘          └─────┘ └┘  └┘
typ  ─────┘ └────────────────────┘└─┘  └┘ └────┘└───┘     └─────┘ └┘  └┘
doc  ─────┘                       └─┘  └┘ └────┘                  └┘  └┘
txt  ─────┘                       └─┘  └┘ └────┘                  └┘  └┘
par  ─────┘                       └─┘  └┘ └────┘                  └┘  └┘
pid  ─────┘                       └─┘  └┘ └────┘                  └┘  └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
165    refine ⟨⟨F, _, _⟩, _⟩,
id              
src    └─────┘   └─────────┘
typ    └─────┘  └─────────┘
doc    └─────┘   └─────────┘
txt    └─────┘   └─────────┘
par    └─────┘   └─────────┘
pid             └─────────┘
st   ──────────────────────┘└─
166    { /- Check that `F` is continuous -/
st   ───┘└──────────────────────────────────
167      refine continuous_of_uniform_limit_of_continuous (λ ε ε0, _) (λN, (f N).2.1),
id              └───────────────────────────────────────┘                   
src      └─────┘└───────────────────────────────────────┘  └────────┘  └─┘   └────┘
typ      └─────┘└───────────────────────────────────────┘  └────────┘  └─┘  └────┘
doc      └─────┘└───────────────────────────────────────┘  └────────┘  └─┘   └────┘
txt      └─────┘                                           └────────┘  └─┘   └────┘
par      └─────┘                                           └────────┘  └─┘   └────┘
pid                                                       └────────┘  └─┘   └────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
168      rcases metric.tendsto_at_top.1 b_lim ε ε0 with ⟨N, hN⟩,
id              └───────────────────┘   └───┘  └┘
src      └─────┘└───────────────────┘└─┘        └───────────┘
typ      └─────┘└───────────────────┘└─┘└───┘└┘└───────────┘
doc      └─────┘                     └─┘        └───────────┘
txt      └─────┘                     └─┘        └───────────┘
par      └─────┘                     └─┘        └───────────┘
pid                                 └─┘        └───────────┘
st   ─────────────────────────────────────────────────────────┘└─
169      exact ⟨N, λy, calc
src      └────┘  └┘ └─┘    
typ      └────┘  └┘ └─┘    
doc      └────┘  └┘ └─┘    
txt      └────┘  └┘ └─┘    
par      └────┘  └┘ └─┘    
pid             └┘ └─┘    
st   ───────────────────────
170        dist (f N y) (F y) ≤ b N : fF_bdd y N
id                                 └────┘
src  ─────┘        └┘   └┘   └─┘        
typ  ─────┘       └┘  └┘  └─┘└────┘  
doc  ─────┘        └┘   └┘   └─┘        
txt  ─────┘        └┘   └┘   └─┘        
par  ─────┘        └┘   └┘   └─┘        
pid  ─────┘        └┘   └┘   └─┘        
st   ────────────────────────────────────────────
171        ... ≤ dist (b N) 0 : begin simp, show b N ≤ abs(b N), from le_abs_self _ end
id               └──┘                                  └─┘          └─────────┘
src  ─────────┘ └──┘   └────┘     └──┘└┘└───┘   └─┘   └┘└───┘└─────────┘└─┘└───
typ  ─────────┘ └──┘   └────┘     └──┘└─────┘   └─┘ └──────┘└─────────┘└──────
doc  ─────────┘        └────┘     └──┘└┘└───┘         └┘└───┘           └─┘└───
txt  ─────────┘        └────┘     └──┘└┘└───┘         └┘└───┘           └─┘└───
par  ─────────┘        └────┘     └──┘└─────┘         └──────┘           └──────
pid  ─────────┘        └────┘     └──────────┘         └──────┘           └──────
st   ──────────────────────────┘└────────┘└───────────────────┘└───────────────────┘└─┘
172        ... ≤ ε : le_of_lt (hN N (le_refl N))⟩ },
id                  └──────┘  └┘    └─────┘ 
src  ─────────┘  └─┘└──────┘     └─────┘ └──┘
typ  ─────────┘ └─┘└──────┘ └┘  └─────┘└──┘
doc  ─────────┘  └─┘                     └──┘
txt  ─────────┘  └─┘                     └──┘
par  ─────────┘  └─┘                     └──┘
pid  ─────────┘  └─┘                     └─┘
st   ────────────────────────────────────────────┘└┘
173    { /- Check that `F` is bounded -/
st   ───┘└───────────────────────────────
174      rcases (f 0).2.2 with ⟨C, hC⟩,
id               
src      └─────┘  └──────────────────┘
typ      └─────┘ └──────────────────┘
doc      └─────┘  └──────────────────┘
txt      └─────┘  └──────────────────┘
par      └─────┘  └──────────────────┘
pid              └──────────────────┘
st   ────────────────────────────────┘└─
175      exact ⟨C + (b 0 + b 0), λ x y, calc
id                
src      └────┘    └─┘  └───┘ └────┘    
typ      └────┘    └─┘  └───┘ └────┘    
doc      └────┘     └─┘  └───┘ └────┘    
txt      └────┘     └─┘  └───┘ └────┘    
par      └────┘     └─┘  └───┘ └────┘    
pid                └─┘  └───┘ └────┘    
st   ────────────────────────────────────────
176        dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) : dist_triangle4_left _ _ _ _
id                                                                         └──┘                └─────────────────┘
src  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘ └──┘  └─┘ └┘   └───┘└─────────────────┘└────────
typ  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘ └──┘ └─┘ └┘  └───┘└─────────────────┘└────────
doc  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘       └─┘ └┘   └───┘                   └────────
txt  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘       └─┘ └┘   └───┘                   └────────
par  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘       └─┘ └┘   └───┘                   └────────
pid  ─────┘       └┘   └┘       └─┘ └┘  └─┘ └┘        └─┘ └┘   └┘       └─┘ └┘   └───┘                   └────────
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
177           ... ≤ C + (b 0 + b 0) : add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))⟩ },
id                                              └┘       └────────┘               └────┘
src  ────────────┘     └─┘  └────┘               └┘ └────────┘        └──┘        └────┘
typ  ────────────┘    └─┘ └────┘           └┘  └┘ └────────┘        └──┘ └────┘ └────┘
doc  ────────────┘     └─┘  └────┘               └┘                   └──┘        └────┘
txt  ────────────┘     └─┘  └────┘               └┘                   └──┘        └────┘
par  ────────────┘     └─┘  └────┘               └┘                   └──┘        └────┘
pid  ────────────┘     └─┘  └────┘               └┘                   └──┘        └───┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└┘
178    { /- Check that `F` is close to `f N` in distance terms -/
st   ─────────────────────────────────────────────────────────────
179      refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (λ _, dist_nonneg) _ b_lim),
id              └───────────────────────────┘    └──────────┘       └─────────┘    └───┘
src      └─────┘└───────────────────────────┘└─┘ └──────────┘  └──┘└─────────┘└──┘     
typ      └─────┘└───────────────────────────┘└─┘ └──────────┘  └──┘└─────────┘└──┘└───┘
doc      └─────┘                             └─┘               └──┘           └──┘     
txt      └─────┘                             └─┘               └──┘           └──┘     
par      └─────┘                             └─┘               └──┘           └──┘     
pid                                         └─┘               └──┘           └──┘     
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
180      exact λ N, (dist_le (b0 _)).2 (λx, fF_bdd x N) }
id                   └─────┘  └┘            └────┘
src      └────┘ └──┘ └─────┘   └─────┘  └─┘        └┘
typ      └────┘ └──┘ └─────┘ └┘└─────┘  └─┘└────┘  └┘
doc      └────┘ └──┘ └─────┘   └─────┘  └─┘        └┘
txt      └────┘ └──┘           └─────┘  └─┘        └┘
par      └────┘ └──┘           └─────┘  └─┘        └┘
pid            └──┘           └─────┘  └─┘        
st   ──────────────────────────────────────────────────┘└─
181  end
st   ──┘
182  
183  /-- Composition (in the target) of a bounded continuous function with a Lipschitz map again
184  gives a bounded continuous function -/
185  def comp (G : β → γ) {C : nnreal} (H : lipschitz_with C G)
id                           └────┘       └────────────┘  
src                            └────┘       └────────────┘
typ                          └────┘       └────────────┘  
doc                            └────┘       └────────────┘
186    (f : α →ᵇ β) : α →ᵇ γ :=
id           └┘      └┘ 
src           └┘        └┘
typ          └┘      └┘ 
doc           └┘        └┘
187  ⟨λx, G (f x), H.to_continuous.comp f.2.1,
id             └────────────┘└───┘  
src                 └────────────┘└───┘   
typ            └────────────┘└───┘  
doc                 └────────────┘
188    let ⟨D, hD⟩ := f.2.2 in
id     └─┘    └┘      
src                     
typ    └─┘    └┘      
189    ⟨max C 0 * D, λ x y, calc
id      └─┘           
src     └─┘     
typ     └─┘           
190      dist (G (f x)) (G (f y)) ≤ C * dist (f x) (f y) : H _ _
id       └──┘                   └──┘           
src      └──┘                          └──┘
typ      └──┘                   └──┘           
191      ... ≤ max C 0 * dist (f x) (f y) : mul_le_mul_of_nonneg_right (le_max_left C 0) dist_nonneg
id             └─┘     └──┘           └────────────────────────┘  └─────────┘     └─────────┘
src            └─┘      └──┘               └────────────────────────┘  └─────────┘      └─────────┘
typ            └─┘     └──┘           └────────────────────────┘  └─────────┘     └─────────┘
192      ... ≤ max C 0 * D : mul_le_mul_of_nonneg_left (hD _ _) (le_max_right C 0)⟩⟩
id             └─┘         └───────────────────────┘           └──────────┘ 
src            └─┘          └───────────────────────┘           └──────────┘
typ            └─┘         └───────────────────────┘           └──────────┘ 
193  
194  /-- The composition operator (in the target) with a Lipschitz map is Lipschitz -/
195  lemma lipschitz_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id                                       └────┘       └────────────┘  
src                                        └────┘       └────────────┘
typ                                      └────┘       └────────────┘  
doc                                        └────┘       └────────────┘
196    lipschitz_with C (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id     └────────────┘   └──┘       └┘      └┘ 
src    └────────────┘    └──┘          └┘        └┘
typ    └────────────┘   └──┘       └┘      └┘ 
doc    └────────────┘    └──┘          └┘        └┘
197  λ f g,
id      
typ     
198  (dist_le (mul_nonneg C.2 dist_nonneg)).2 $ λ x,
id    └─────┘  └────────┘   └─────────┘        
src   └─────┘  └────────┘    └─────────┘  
typ   └─────┘  └────────┘   └─────────┘        
doc   └─────┘
199  calc dist (G (f x)) (G (g x)) ≤ C * dist (f x) (g x) : H _ _
id        └──┘                   └──┘           
src       └──┘                          └──┘
typ       └──┘                   └──┘           
200    ... ≤ C * dist f g : mul_le_mul_of_nonneg_left (dist_coe_le_dist _) C.2
id             └──┘     └───────────────────────┘  └──────────────┘    
src             └──┘       └───────────────────────┘  └──────────────┘     
typ            └──┘     └───────────────────────┘  └──────────────┘    
doc                                                    └──────────────┘
201  
202  /-- The composition operator (in the target) with a Lipschitz map is uniformly continuous -/
203  lemma uniform_continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id                                                └────┘       └────────────┘  
src                                                 └────┘       └────────────┘
typ                                               └────┘       └────────────┘  
doc                                                 └────┘       └────────────┘
204    uniform_continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id     └────────────────┘  └──┘       └┘      └┘ 
src    └────────────────┘  └──┘          └┘        └┘
typ    └────────────────┘  └──┘       └┘      └┘ 
doc                        └──┘          └┘        └┘
205  (lipschitz_comp H).to_uniform_continuous
id    └────────────┘  └───────────────────┘
src   └────────────┘   └───────────────────┘
typ   └────────────┘  └───────────────────┘
doc   └────────────┘   └───────────────────┘
206  
207  /-- The composition operator (in the target) with a Lipschitz map is continuous -/
208  lemma continuous_comp {G : β → γ} {C : nnreal} (H : lipschitz_with C G) :
id                                        └────┘       └────────────┘  
src                                         └────┘       └────────────┘
typ                                       └────┘       └────────────┘  
doc                                         └────┘       └────────────┘
209    continuous (comp G H : (α →ᵇ β) → α →ᵇ γ) :=
id     └────────┘  └──┘       └┘      └┘ 
src    └────────┘  └──┘          └┘        └┘
typ    └────────┘  └──┘       └┘      └┘ 
doc    └────────┘  └──┘          └┘        └┘
210  (lipschitz_comp H).to_continuous
id    └────────────┘  └───────────┘
src   └────────────┘   └───────────┘
typ   └────────────┘  └───────────┘
doc   └────────────┘   └───────────┘
211  
212  /-- Restriction (in the target) of a bounded continuous function taking values in a subset -/
213  def cod_restrict (s : set β) (f : α →ᵇ β) (H : ∀x, f x ∈ s) : α →ᵇ s :=
id                         └─┘         └┘                   └┘ 
src                        └─┘           └┘                         └┘
typ                        └─┘         └┘                   └┘ 
doc                                      └┘                          └┘
214  ⟨λx, ⟨f x, H x⟩, continuous_subtype_mk _ f.2.1, f.2.2⟩
id               └───────────────────┘        
src                   └───────────────────┘          
typ              └───────────────────┘        
215  
216  end basics
217  
218  section arzela_ascoli
219  variables [topological_space α] [compact_space α] [metric_space β]
id             └───────────────┘     └───────────┘     └──────────┘
src             └───────────────┘     └───────────┘     └──────────┘
typ            └───────────────┘     └───────────┘     └──────────┘
doc             └───────────────┘     └───────────┘     └──────────┘
220  variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id                      └┘                 
src                     └┘                 
typ                     └┘                 
doc                     └┘
221  
222  /- Arzela-Ascoli theorem asserts that, on a compact space, a set of functions sharing
223  a common modulus of continuity and taking values in a compact set forms a compact
224  subset for the topology of uniform convergence. In this section, we prove this theorem
225  and several useful variations around it. -/
226  
227  /-- First version, with pointwise equicontinuity and range in a compact space -/
228  theorem arzela_ascoli₁ [compact_space β]
id                           └───────────┘ 
src                          └───────────┘
typ                          └───────────┘ 
doc                          └───────────┘
229    (A : set (α →ᵇ β))
id          └─┘   └┘ 
src         └─┘    └┘
typ         └─┘   └┘ 
doc                └┘
230    (closed : is_closed A)
id               └───────┘ 
src              └───────┘
typ              └───────┘ 
doc              └───────┘
231    (H : ∀ (x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id                                           └┘ 
src                                                    └┘
typ                                          └┘ 
doc                                                      └┘
232      f ∈ A → dist (f y) (f z) < ε) :
id            └──┘          
src             └──┘             
typ           └──┘          
233    compact A :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
doc    └─────┘
234  begin
st   └─────
235    refine compact_of_totally_bounded_is_closed _ closed,
id            └──────────────────────────────────┘   └────┘
src    └─────┘└──────────────────────────────────┘└─┘
typ    └─────┘└──────────────────────────────────┘└─┘└────┘
doc    └─────┘                                    └─┘
txt    └─────┘                                    └─┘
par    └─────┘                                    └─┘
pid                                              └─┘
st   ─────────────────────────────────────────────────────┘└─
236    refine totally_bounded_of_finite_discretization (λ ε ε0, _),
id            └──────────────────────────────────────┘
src    └─────┘└──────────────────────────────────────┘  └───────┘
typ    └─────┘└──────────────────────────────────────┘  └───────┘
doc    └─────┘└──────────────────────────────────────┘  └───────┘
txt    └─────┘                                          └───────┘
par    └─────┘                                          └───────┘
pid                                                    └───────┘
st   ────────────────────────────────────────────────────────────┘└─
237    rcases dense ε0 with ⟨ε₁, ε₁0, εε₁⟩,
id            └───┘ └┘
src    └─────┘└───┘  └──────────────────┘
typ    └─────┘└───┘└┘└──────────────────┘
doc    └─────┘       └──────────────────┘
txt    └─────┘       └──────────────────┘
par    └─────┘       └──────────────────┘
pid                 └──────────────────┘
st   ────────────────────────────────────┘└─
238    let ε₂ := ε₁/2/2,
id               └┘
src    └────────┘   
typ    └────────┘└┘ 
doc    └────────┘    
txt    └────────┘    
par    └────────┘    
pid    └────┘└─┘    
st   ─────────────────┘└─
239    /- We have to find a finite discretization of `u`, i.e., finite information
st   ──────────────────────────────────────────────────────────────────────────────
240    that is sufficient to reconstruct `u` up to ε. This information will be
st   ──────────────────────────────────────────────────────────────────────────
241    provided by the values of `u` on a sufficiently dense set tα,
st   ────────────────────────────────────────────────────────────────
242    slightly translated to fit in a finite ε₂-dense set tβ in the image. Such
st   ────────────────────────────────────────────────────────────────────────────
243    sets exist by compactness of the source and range. Then, to check that these
st   ───────────────────────────────────────────────────────────────────────────────
244    data determine the function up to ε, one uses the control on the modulus of
st   ──────────────────────────────────────────────────────────────────────────────
245    continuity to extend the closeness on tα to closeness everywhere. -/
st   ───────────────────────────────────────────────────────────────────────
246    have ε₂0 : ε₂ > 0 := half_pos (half_pos ε₁0),
id                └┘                 └──────┘ └─┘
src    └─────────┘  └────┘         └──────┘   
typ    └─────────┘└┘└────┘         └──────┘└─┘
doc    └─────────┘   └────┘                    
txt    └─────────┘   └────┘                    
par    └─────────┘   └────┘                    
pid    └──────┘└─┘   └───┘                    
st   ─────────────────────────────────────────────┘└─
247    have : ∀x:α, ∃U, x ∈ U ∧ is_open U ∧ ∀ (y z ∈ U) {f : α →ᵇ β},
id                            └─────┘                       └┘ 
src    └─────┘ └┘      └─────┘   └──────┘ └─────┘ └┘  
typ    └─────┘ └┘      └─────┘   └──────┘ └─────┘└┘ 
doc    └─────┘ └┘        └─────┘   └──────┘ └─────┘ └┘  
txt    └─────┘ └┘                  └──────┘ └─────┘     
par    └─────┘ └┘                  └──────┘ └─────┘     
pid    └───┘└┘ └┘                  └──────┘ └─────┘     
st   ─────────────────────────────────────────────────────────────────
248      f ∈ A → dist (f y) (f z) < ε₂ := λ x,
id             └──┘              └┘
src  ───┘    └──┘   └┘   └┘  └──┘ └───
typ  ───┘  └──┘   └┘   └┘└┘└──┘ └───
doc  ───┘           └┘   └┘   └──┘ └───
txt  ───┘           └┘   └┘   └──┘ └───
par  ───┘           └┘   └┘   └──┘ └───
pid  ───┘           └┘   └┘   └──┘ └───
st   ──────────────────────────────────────────
249        let ⟨U, nhdsU, hU⟩ := H x _ ε₂0,
id                 └───┘  └┘          └─┘
src  ─────┘     └┘     └┘  └───┘  └─┘   └─
typ  ─────┘     └┘└───┘└┘└┘└───┘ └─┘└─┘└─
doc  ─────┘     └┘     └┘  └───┘  └─┘   └─
txt  ─────┘     └┘     └┘  └───┘  └─┘   └─
par  ─────┘     └┘     └┘  └───┘  └─┘   └─
pid  ─────┘     └┘     └┘  └───┘  └─┘   └─
st   ───────────────────────────────────────
250            ⟨V, VU, openV, xV⟩ := mem_nhds_sets_iff.1 nhdsU in
id                └┘  └───┘  └┘     └───────────────┘
src  ─────────┘  └┘  └┘     └┘  └───┘└───────────────┘└─┘     └───
typ  ─────────┘ └┘└┘└┘└───┘└┘└┘└───┘└───────────────┘└─┘     └───
doc  ─────────┘  └┘  └┘     └┘  └───┘                 └─┘     └───
txt  ─────────┘  └┘  └┘     └┘  └───┘                 └─┘     └───
par  ─────────┘  └┘  └┘     └┘  └───┘                 └─┘     └───
pid  ─────────┘  └┘  └┘     └┘  └───┘                 └─┘     └───
st   ─────────────────────────────────────────────────────────────
251        ⟨V, xV, openV, λy z hy hz f hf, hU y z (VU hy) (VU hz) f hf⟩,
src  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
typ  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
doc  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
txt  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
par  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
pid  ─────┘  └┘  └┘     └┘ └──────────────┘         └┘     └┘   
st   ─────────────────────────────────────────────────────────────────┘└─
252    choose U hU using this,
id                       └──┘
src    └────────────────┘
typ    └────────────────┘└──┘
doc    └────────────────┘
txt    └────────────────┘
par    └────────────────┘
pid          └┘└─┘└─────┘
st   ───────────────────────┘└─
253    /- For all x, the set hU x is an open set containing x on which the elements of A
st   ────────────────────────────────────────────────────────────────────────────────────
254    fluctuate by at most ε₂.
st   ───────────────────────────
255    We extract finitely many of these sets that cover the whole space, by compactness -/
st   ───────────────────────────────────────────────────────────────────────────────────────
256    rcases compact_univ.elim_finite_subcover_image
id            └─────────────────────────────────────┘
src    └─────┘└─────────────────────────────────────┘
typ    └─────┘└─────────────────────────────────────┘
doc    └─────┘                                       
txt    └─────┘                                       
par    └─────┘                                       
pid                                                 
st   ─────────────────────────────────────────────────
257      (λx _, (hU x).2.1) (λx hx, mem_bUnion (mem_univ _) (hU x).1)
id                                  └────────┘  └──────┘     └┘
src  ───┘  └───┘    └─────┘  └────┘└────────┘ └──────┘└──┘    └────
typ  ───┘  └───┘    └─────┘  └────┘└────────┘ └──────┘└──┘ └┘ └────
doc  ───┘  └───┘    └─────┘  └────┘                   └──┘    └────
txt  ───┘  └───┘    └─────┘  └────┘                   └──┘    └────
par  ───┘  └───┘    └─────┘  └────┘                   └──┘    └────
pid  ───┘  └───┘    └─────┘  └────┘                   └──┘    └────
st   ─────────────────────────────────────────────────────────────────
258      with ⟨tα, _, ⟨_⟩, htα⟩,
src  ─────────────────────────┘
typ  ─────────────────────────┘
doc  ─────────────────────────┘
txt  ─────────────────────────┘
par  ─────────────────────────┘
pid  ─────────────────────────┘
st   ─────────────────────────┘└─
259    /- tα : set α, htα : univ ⊆ ⋃x ∈ tα, U x -/
st   ──────────────────────────────────────────────
260    rcases @finite_cover_balls_of_compact β _ _ compact_univ _ ε₂0
id             └───────────────────────────┘      └──────────┘   └─┘
src    └─────┘ └───────────────────────────┘ └───┘└──────────┘└─┘   
typ    └─────┘ └───────────────────────────┘└───┘└──────────┘└─┘└─┘
doc    └─────┘ └───────────────────────────┘ └───┘            └─┘   
txt    └─────┘                               └───┘            └─┘   
par    └─────┘                               └───┘            └─┘   
pid                                         └───┘            └─┘   
st   ─────────────────────────────────────────────────────────────────
261      with ⟨tβ, _, ⟨_⟩, htβ⟩, resetI,
src  ─────────────────────────┘  └────┘
typ  ─────────────────────────┘  └────┘
doc  ─────────────────────────┘  └────┘
txt  ─────────────────────────┘  └────┘
par  ─────────────────────────┘  └────┘
pid  ─────────────────────────┘
st   ─────────────────────────┘└─────────
262    /- tβ : set β, htβ : univ ⊆ ⋃y ∈ tβ, ball y ε₂ -/
st   ────────────────────────────────────────────────────
263    /- Associate to every point `y` in the space a nearby point `F y` in tβ -/
st   ─────────────────────────────────────────────────────────────────────────────
264    choose F hF using λy, show ∃z∈tβ, dist y z < ε₂, by simpa using htβ (mem_univ y),
id                                  └┘ └──┘       └┘                 └─┘  └──────┘ 
src    └────────────────┘ └─┘    └┘  └──┘     └───┘└──────────┘    └──────┘ 
typ    └────────────────┘ └─┘    └┘└┘└──┘   └┘└───┘└──────────┘└─┘ └──────┘
doc    └────────────────┘ └─┘     └┘            └───┘└──────────┘             
txt    └────────────────┘ └─┘     └┘            └───┘└──────────┘             
par    └────────────────┘ └─┘     └┘            └───┘└──────────┘             
pid          └┘└─┘└─────┘ └─┘     └┘            └───────────────┘             
st   ────────────────────────────────────────────────────┘└───────────────────────────┘└─
265    /- F : β → β, hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂ -/
st   ────────────────────────────────────────────────────────────────
266  
st   
267    /- Associate to every function a discrete approximation, mapping each point in `tα`
st   ──────────────────────────────────────────────────────────────────────────────────────
268    to a point in `tβ` close to its true image by the function. -/
st   ─────────────────────────────────────────────────────────────────
269    refine ⟨tα → tβ, by apply_instance, λ f a, ⟨F (f a), (hF (f a)).1⟩, _⟩,
id             └┘  └┘                                      └┘
src    └─────┘      └┘  └────────────┘└┘ └────┘     └─┘      └───────┘
typ    └─────┘ └┘└┘└┘  └────────────┘└┘ └────┘    └─┘ └┘   └───────┘
doc    └─────┘      └┘  └────────────┘└┘ └────┘     └─┘      └───────┘
txt    └─────┘      └┘  └────────────┘└┘ └────┘     └─┘      └───────┘
par    └─────┘      └┘  └────────────┘└┘ └────┘     └─┘      └───────┘
pid                └┘  └───────────────┘ └────┘     └─┘      └───────┘
st   ────────────────────┘└─────────────┘└──────────────────────────────────┘└─
270    rintro ⟨f, hf⟩ ⟨g, hg⟩ f_eq_g,
src    └───────────────────────────┘
typ    └───────────────────────────┘
doc    └───────────────────────────┘
txt    └───────────────────────────┘
par    └───────────────────────────┘
pid          └─────────────────────┘
st   ──────────────────────────────┘└─
271    /- If two functions have the same approximation, then they are within distance ε -/
st   ──────────────────────────────────────────────────────────────────────────────────────
272    refine lt_of_le_of_lt ((dist_le $ le_of_lt ε₁0).2 (λ x, _)) εε₁,
id            └────────────┘   └─────┘   └──────┘ └─┘              └─┘
src    └─────┘└────────────┘  └─────┘ └──────┘   └──┘  └──────┘
typ    └─────┘└────────────┘  └─────┘ └──────┘└─┘└──┘  └──────┘└─┘
doc    └─────┘                └─────┘            └──┘  └──────┘
txt    └─────┘                                   └──┘  └──────┘
par    └─────┘                                   └──┘  └──────┘
pid                                             └──┘  └──────┘
st   ────────────────────────────────────────────────────────────────┘└─
273    obtain ⟨x', x'tα, hx'⟩ : ∃x' ∈ tα, x ∈ U x' := mem_bUnion_iff.1 (htα (mem_univ x)),
id                                    └┘             └────────────┘    └─┘  └──────┘ 
src    └───────────────────────┘ └───┘        └──┘└────────────┘└─┘     └──────┘ └┘
typ    └───────────────────────┘ └───┘└┘     └──┘└────────────┘└─┘ └─┘ └──────┘└┘
doc    └───────────────────────┘ └───┘        └──┘              └─┘              └┘
txt    └───────────────────────┘ └───┘        └──┘              └─┘              └┘
par    └───────────────────────┘ └───┘        └──┘              └─┘              └┘
pid          └─────────────────┘ └───┘        └──┘              └─┘              └┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
274    refine calc dist (f x) (g x)
src    └─────┘           └┘   └─
typ    └─────┘           └┘   └─
doc    └─────┘           └┘   └─
txt    └─────┘           └┘   └─
par    └─────┘           └┘   └─
pid                     └┘   └─
st   ───────────────────────────────
275        ≤ dist (f x) (f x') + dist (g x) (g x') + dist (f x') (g x') : dist_triangle4_right _ _ _ _
id                                                  └──┘         └┘    └──────────────────┘
src  ─────┘        └┘    └┘        └┘    └┘ └──┘    └┘    └──┘└──────────────────┘└────────
typ  ─────┘        └┘    └┘       └┘    └┘ └──┘   └┘ └┘└──┘└──────────────────┘└────────
doc  ─────┘        └┘    └┘        └┘    └┘         └┘    └──┘                    └────────
txt  ─────┘        └┘    └┘        └┘    └┘         └┘    └──┘                    └────────
par  ─────┘        └┘    └┘        └┘    └┘         └┘    └──┘                    └────────
pid  ─────┘        └┘    └┘        └┘    └┘         └┘    └──┘                    └────────
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
276    ... ≤ ε₂ + ε₂ + ε₁/2 : le_of_lt (add_lt_add (add_lt_add _ _) _)
id                └┘         └──────┘              └────────┘
src  ─────┘         └──┘└──────┘            └────────┘└────────
typ  ─────┘    └┘   └──┘└──────┘            └────────┘└────────
doc  ─────┘          └──┘                              └────────
txt  ─────┘          └──┘                              └────────
par  ─────┘          └──┘                              └────────
pid  ─────┘          └──┘                              └────────
st   ──────────────────────────────────────────────────────────────────
277    ... = ε₁ : by rw [add_halves, add_halves],
id           └┘          └────────┘  └────────┘
src  ─────┘   └─┘  └──┘└────────┘└┘└────────┘
typ  ─────┘ └┘└─┘  └──┘└────────┘└┘└────────┘
doc  ─────┘   └─┘  └──┘          └┘          
txt  ─────┘   └─┘  └──┘          └┘          
par  ─────┘   └─┘  └──┘          └┘          
pid  ─────┘   └─┘  └───┘          └┘          
st   ──────────────┘└─────────────┘└──────────┘└─
278    { exact (hU x').2.2 _ _ hx' ((hU x').1) hf },
id                             └─┘   └┘ └┘     └┘
src      └────┘     └────────┘         └───┘  
typ      └────┘     └────────┘└─┘  └┘└┘└───┘└┘
doc      └────┘     └────────┘         └───┘  
txt      └────┘     └────────┘         └───┘  
par      └────┘     └────────┘         └───┘  
pid                └────────┘         └───┘  
st   ───┘└───────────────────────────────────────┘└┘
279    { exact (hU x').2.2 _ _ hx' ((hU x').1) hg },
id                             └─┘   └┘ └┘     └┘
src      └────┘     └────────┘         └───┘  
typ      └────┘     └────────┘└─┘  └┘└┘└───┘└┘
doc      └────┘     └────────┘         └───┘  
txt      └────┘     └────────┘         └───┘  
par      └────┘     └────────┘         └───┘  
pid                └────────┘         └───┘  
st   ───┘└───────────────────────────────────────┘└┘
280    { have F_f_g : F (f x') = F (g x') :=
id                                └┘
src      └───────────┘     └┘     └────
typ      └───────────┘    └┘ └┘└────
doc      └───────────┘     └┘      └────
txt      └───────────┘     └┘      └────
par      └───────────┘     └┘      └────
pid      └────────┘└─┘     └┘      └───
st   ────────────────────────────────────────
281        (congr_arg (λ f:tα → tβ, (f ⟨x', x'tα⟩ : β)) f_eq_g : _),
id          └───────┘      └┘   └┘      └┘  └──┘       └────┘
src  ─────┘ └───────┘  └─┘     └┘     └┘    └──┘ └─┘      └───┘
typ  ─────┘ └───────┘  └─┘└┘ └┘└┘   └┘└┘└──┘└──┘└─┘└────┘└───┘
doc  ─────┘            └─┘     └┘     └┘    └──┘ └─┘      └───┘
txt  ─────┘            └─┘     └┘     └┘    └──┘ └─┘      └───┘
par  ─────┘            └─┘     └┘     └┘    └──┘ └─┘      └───┘
pid  ─────┘            └─┘     └┘     └┘    └──┘ └─┘      └───┘
st   ─────────────────────────────────────────────────────────────┘└─
282      calc dist (f x') (g x')
id       └──┘
src      └──┘
typ      └──┘
doc      └──┘
st   ────────────────────────────
283            ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) : dist_triangle_right _ _ _
id                                        └──┘                    └─────────────────┘
src                                       └──┘                     └─────────────────┘
typ                                       └──┘                    └─────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────
284        ... = dist (f x') (F (f x')) + dist (g x') (F (g x')) : by rw F_f_g
id                                                                       └───┘
src                                                                   └─┘     
typ                                                                   └─┘└───┘
doc                                                                   └─┘     
txt                                                                   └─┘     
par                                                                   └─┘     
pid                                                                          
st   ───────────────────────────────────────────────────────────────┘└─────────
285        ... < ε₂ + ε₂ : add_lt_add (hF (f x')).2 (hF (g x')).2
id                    └┘   └────────┘              └┘   └┘  
src  ─────┘                └────────┘                         
typ  ─────┘           └┘   └────────┘              └┘   └┘  
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└──────────────────────────────────────────────────────
286        ... = ε₁/2 : add_halves _ }
id               └┘     └────────┘
src                     └────────┘
typ              └┘     └────────┘
st   ──────────────────────────────┘└──
287  end
st   ──┘
288  
289  /-- Second version, with pointwise equicontinuity and range in a compact subset -/
290  theorem arzela_ascoli₂
291    (s : set β) (hs : compact s)
id          └─┘         └─────┘ 
src         └─┘          └─────┘
typ         └─┘         └─────┘ 
doc                      └─────┘
292    (A : set (α →ᵇ β))
id          └─┘   └┘ 
src         └─┘    └┘
typ         └─┘   └┘ 
doc                └┘
293    (closed : is_closed A)
id               └───────┘ 
src              └───────┘
typ              └───────┘ 
doc              └───────┘
294    (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
id                    └┘                   
src                    └┘                        
typ                   └┘                   
doc                    └┘
295    (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id                                          └┘ 
src                                                   └┘
typ                                         └┘ 
doc                                                     └┘
296      f ∈ A → dist (f y) (f z) < ε) :
id            └──┘          
src             └──┘             
typ           └──┘          
297    compact A :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
doc    └─────┘
298  /- This version is deduced from the previous one by restricting to the compact type in the target,
299  using compactness there and then lifting everything to the original space. -/
300  begin
st   └─────
301    have M : lipschitz_with 1 coe := lipschitz_with.subtype_coe s,
id              └────────────┘   └─┘    └────────────────────────┘ 
src    └───────┘└────────────┘└─┘└─┘└──┘└────────────────────────┘
typ    └───────┘└────────────┘└─┘└─┘└──┘└────────────────────────┘
doc    └───────┘└────────────┘└─┘   └──┘                          
txt    └───────┘              └─┘   └──┘                          
par    └───────┘              └─┘   └──┘                          
pid    └────┘└─┘              └─┘   └──┘                          
st   ──────────────────────────────────────────────────────────────┘└─
302    let F : (α →ᵇ s) → α →ᵇ β := comp coe M,
id                └┘             └──┘ └─┘ 
src    └──────┘  └┘ └┘     └──┘└──┘└─┘
typ    └──────┘  └┘└┘   └──┘└──┘└─┘
doc    └──────┘  └┘ └┘     └──┘└──┘   
txt    └──────┘     └┘     └──┘       
par    └──────┘     └┘     └──┘       
pid    └───┘└─┘     └┘     └──┘       
st   ────────────────────────────────────────┘└─
303    refine compact_of_is_closed_subset
id            └─────────────────────────┘
src    └─────┘└─────────────────────────┘
typ    └─────┘└─────────────────────────┘
doc    └─────┘                           
txt    └─────┘                           
par    └─────┘                           
pid                                     
st   ─────────────────────────────────────
304      ((_ : compact (F ⁻¹' A)).image (continuous_comp M)) closed (λ f hf, _),
id             └─────┘   └─┘           └─────────────┘    └────┘
src  ───┘  └──┘└─────┘  └─┘ └───────┘ └─────────────┘ └─┘        └───────┘
typ  ───┘  └──┘└─────┘ └─┘└───────┘ └─────────────┘└─┘└────┘  └───────┘
doc  ───┘  └──┘└─────┘  └─┘ └───────┘ └─────────────┘ └─┘        └───────┘
txt  ───┘  └──┘             └───────┘                 └─┘        └───────┘
par  ───┘  └──┘             └───────┘                 └─┘        └───────┘
pid  ───┘  └──┘             └───────┘                 └─┘        └───────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
305    { haveI : compact_space s := compact_iff_compact_space.1 hs,
id               └───────────┘     └───────────────────────┘   └┘
src      └──────┘└───────────┘ └──┘└───────────────────────┘└─┘
typ      └──────┘└───────────┘└──┘└───────────────────────┘└─┘└┘
doc      └──────┘└───────────┘ └──┘                         └─┘
txt      └──────┘              └──┘                         └─┘
par      └──────┘              └──┘                         └─┘
pid           └┘              └──┘                         └─┘
st   ───┘└───────────────────────────────────────────────────────┘└─
306      refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed)
id              └────────────┘    └──────────────────────┘    └─────────────┘     └────┘
src      └─────┘└────────────┘└─┘ └──────────────────────┘└─┘ └─────────────┘ └──┘      └─
typ      └─────┘└────────────┘└─┘ └──────────────────────┘└─┘ └─────────────┘└──┘└────┘└─
doc      └─────┘└────────────┘└─┘                         └─┘ └─────────────┘ └──┘      └─
txt      └─────┘              └─┘                         └─┘                 └──┘      └─
par      └─────┘              └─┘                         └─┘                 └──┘      └─
pid                          └─┘                         └─┘                 └──┘      └─
st   ──────────────────────────────────────────────────────────────────────────────────────
307        (λ x ε ε0, bex.imp_right (λ U U_nhds hU y z hy hz f hf, _) (H x ε ε0)),
id                    └───────────┘                                    
src  ─────┘  └───────┘└───────────┘  └──────────────────────────────┘      └┘
typ  ─────┘  └───────┘└───────────┘  └──────────────────────────────┘     └┘
doc  ─────┘  └───────┘               └──────────────────────────────┘      └┘
txt  ─────┘  └───────┘               └──────────────────────────────┘      └┘
par  ─────┘  └───────┘               └──────────────────────────────┘      └┘
pid  ─────┘  └───────┘               └──────────────────────────────┘      └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
308      calc dist (f y) (f z) = dist (F f y) (F f z) : rfl
id       └──┘                    └──┘                   └─┘
src      └──┘                    └──┘                   └─┘
typ      └──┘                    └──┘                   └─┘
doc      └──┘
st   ───────────────────────────────────────────────────────
309                          ... < ε : hU y z hy hz (F f) hf },
id                                    └┘   └┘ └┘     └┘
typ                                   └┘   └┘ └┘     └┘
st   ──────────────────────────────────────────────────────┘└─┘
310    { let g := cod_restrict s f (λx, in_s f x hf),
id                └──────────┘         └──┘    └┘
src      └───────┘└──────────┘    └─┘        
typ      └───────┘└──────────┘   └─┘└──┘ └┘
doc      └───────┘└──────────┘    └─┘        
txt      └───────┘                └─┘        
par      └───────┘                └─┘        
pid      └───┘└─┘                └─┘        
st   ──────────────────────────────────────────────┘└─
311      rw [show f = F g, by ext; refl] at hf ⊢,
id                   
src      └──┘       └───┘└─┘└┘└──┘└───────┘
typ      └──┘    └───┘└─┘└┘└──┘└───────┘
doc      └──┘        └───┘└─┘└┘└──┘└───────┘
txt      └──┘        └───┘└─┘└┘└──┘└───────┘
par      └──┘        └───┘└─┘└┘└──┘└───────┘
pid        └┘        └─────────────┘└──────┘
st   ───────────────────────┘└────────┘└──────┘└─
312      exact ⟨g, hf, rfl⟩ }
id                └┘  └─┘
src      └────┘  └┘  └┘└─┘└┘
typ      └────┘ └┘└┘└┘└─┘└┘
doc      └────┘  └┘  └┘   └┘
txt      └────┘  └┘  └┘   └┘
par      └────┘  └┘  └┘   └┘
pid             └┘  └┘   
st   ──────────────────────┘└─
313  end
st   ──┘
314  
315  /-- Third (main) version, with pointwise equicontinuity and range in a compact subset, but
316  without closedness. The closure is then compact -/
317  theorem arzela_ascoli
318    (s : set β) (hs : compact s)
id          └─┘         └─────┘ 
src         └─┘          └─────┘
typ         └─┘         └─────┘ 
doc                      └─────┘
319    (A : set (α →ᵇ β))
id          └─┘   └┘ 
src         └─┘    └┘
typ         └─┘   └┘ 
doc                └┘
320    (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
id                    └┘                   
src                    └┘                        
typ                   └┘                   
doc                    └┘
321    (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id                                          └┘ 
src                                                   └┘
typ                                         └┘ 
doc                                                     └┘
322      f ∈ A → dist (f y) (f z) < ε) :
id            └──┘          
src             └──┘             
typ           └──┘          
323    compact (closure A) :=
id     └─────┘  └─────┘ 
src    └─────┘  └─────┘
typ    └─────┘  └─────┘ 
doc    └─────┘  └─────┘
324  /- This version is deduced from the previous one by checking that the closure of A, in
325  addition to being closed, still satisfies the properties of compact range and equicontinuity -/
326  arzela_ascoli₂ s hs (closure A) is_closed_closure
id   └────────────┘  └┘  └─────┘   └───────────────┘
src  └────────────┘       └─────┘    └───────────────┘
typ  └────────────┘  └┘  └─────┘   └───────────────┘
doc  └────────────┘       └─────┘
327    (λ f x hf, (mem_of_closed' (closed_of_compact _ hs)).2 $ λ ε ε0,
id          └┘   └────────────┘  └───────────────┘   └┘         └┘
src                └────────────┘  └───────────────┘       
typ         └┘   └────────────┘  └───────────────┘   └┘         └┘
328      let ⟨g, gA, dist_fg⟩ := mem_closure_iff'.1 hf ε ε0 in
id       └─┘    └┘  └─────┘     └──────────────┘  └┘  └┘
src                              └──────────────┘
typ      └─┘    └┘  └─────┘     └──────────────┘  └┘  └┘
doc                              └──────────────┘
329      ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
id            └──┘        └────────────┘  └──────────────┘
src                         └────────────┘  └──────────────┘
typ           └──┘        └────────────┘  └──────────────┘
doc                                         └──────────────┘
330    (λ x ε ε0, show ∃ U ∈ 𝓝 x,
id          └┘            
src                           
typ         └┘            
doc                          
331        ∀ y z ∈ U, ∀ (f : α →ᵇ β), f ∈ closure A → dist (f y) (f z) < ε,
id                         └┘      └─────┘    └──┘          
src                            └┘        └─────┘     └──┘             
typ                        └┘      └─────┘    └──┘          
doc                            └┘         └─────┘
332      begin
st       └─────
333        refine bex.imp_right (λ U U_set hU y z hy hz f hf, _) (H x (ε/2) (half_pos ε0)),
id                └───────────┘                                          └──────┘ └┘
src        └─────┘└───────────┘  └─────────────────────────────┘     └─┘ └──────┘  └┘
typ        └─────┘└───────────┘  └─────────────────────────────┘  └─┘ └──────┘└┘└┘
doc        └─────┘               └─────────────────────────────┘      └─┘           └┘
txt        └─────┘               └─────────────────────────────┘      └─┘           └┘
par        └─────┘               └─────────────────────────────┘      └─┘           └┘
pid                             └─────────────────────────────┘      └─┘           └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
334        rcases mem_closure_iff'.1 hf (ε/2/2) (half_pos (half_pos ε0)) with ⟨g, gA, dist_fg⟩,
id                └──────────────┘   └┘                   └──────┘ └┘
src        └─────┘└──────────────┘└─┘      └─┘          └──────┘  └──────────────────────┘
typ        └─────┘└──────────────┘└─┘└┘   └─┘          └──────┘└┘└──────────────────────┘
doc        └─────┘└──────────────┘└─┘      └─┘                    └──────────────────────┘
txt        └─────┘                └─┘      └─┘                    └──────────────────────┘
par        └─────┘                └─┘      └─┘                    └──────────────────────┘
pid                              └─┘      └─┘                    └──────────────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
335        replace dist_fg := λ x, lt_of_le_of_lt (dist_coe_le_dist x) dist_fg,
id                                 └────────────┘  └──────────────┘    └─────┘
src        └─────────────────┘ └──┘└────────────┘ └──────────────┘ └┘
typ        └─────────────────┘ └──┘└────────────┘ └──────────────┘ └┘└─────┘
doc        └─────────────────┘ └──┘               └──────────────┘ └┘
txt        └─────────────────┘ └──┘                                └┘
par        └─────────────────┘ └──┘                                └┘
pid               └──────┘└─┘ └──┘                                └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
336        calc dist (f y) (f z) ≤ dist (f y) (g y) + dist (f z) (g z) + dist (g y) (g z) : dist_triangle4_right _ _ _ _
id         └──┘                                                         └──┘               └──────────────────┘
src        └──┘                                                          └──┘               └──────────────────┘
typ        └──┘                                                         └──┘               └──────────────────┘
doc        └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
337            ... < ε/2/2 + ε/2/2 + ε/2 :
id                                 
src                                
typ                                
st   ──────────────────────────────────────
338              add_lt_add (add_lt_add (dist_fg y) (dist_fg z)) (hU y z hy hz g gA)
id                           └────────┘              └─────┘      └┘   └┘ └┘  └┘
src                          └────────┘
typ                          └────────┘              └─────┘      └┘   └┘ └┘  └┘
st   ────────────────────────────────────────────────────────────────────────────────
339            ... = ε : by rw [add_halves, add_halves]
id                             └────────┘  └────────┘
src                         └──┘└────────┘└┘└────────┘└─
typ                        └──┘└────────┘└┘└────────┘└─
doc                         └──┘          └┘          └─
txt                         └──┘          └┘          └─
par                         └──┘          └┘          └─
pid                           └┘          └┘          
st   ─────────────────────┘└─────────────┘└──────────┘
340      end)
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
341  
342  /- To apply the previous theorems, one needs to check the equicontinuity. An important
343  instance is when the source space is a metric space, and there is a fixed modulus of continuity
344  for all the functions in the set A -/
345  
346  lemma equicontinuous_of_continuity_modulus {α : Type u} [metric_space α]
id                                                            └──────────┘ 
src                                                           └──────────┘
typ                                                           └──────────┘ 
doc                                                           └──────────┘
347    (b : ℝ → ℝ) (b_lim : tendsto b (𝓝 0) (𝓝 0))
id                        └─────┘        
src                       └─────┘         
typ                       └─────┘        
doc                         └─────┘         
348    (A : set (α →ᵇ β))
id          └─┘   └┘ 
src         └─┘    └┘
typ         └─┘   └┘ 
doc                └┘
349    (H : ∀(x y:α) (f : α →ᵇ β), f ∈ A → dist (f x) (f y) ≤ b (dist x y))
id                        └┘         └──┘            └──┘  
src                         └┘            └──┘                 └──┘
typ                       └┘         └──┘            └──┘  
doc                         └┘
350    (x:α) (ε : ℝ) (ε0 : ε > 0) : ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
id                                                 └┘ 
src                                                         └┘
typ                                                └┘ 
doc                                                             └┘
351      f ∈ A → dist (f y) (f z) < ε :=
id            └──┘          
src             └──┘             
typ           └──┘          
352  begin
st   └─────
353    rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩,
id            └───────────────┘   └───┘  └┘
src    └─────┘└───────────────┘└─┘        └───────────────┘
typ    └─────┘└───────────────┘└─┘└───┘└┘└───────────────┘
doc    └─────┘                 └─┘        └───────────────┘
txt    └─────┘                 └─┘        └───────────────┘
par    └─────┘                 └─┘        └───────────────┘
pid                           └─┘        └───────────────┘
st   ───────────────────────────────────────────────────────┘└─
354    refine ⟨ball x (δ/2), ball_mem_nhds x (half_pos δ0), λ y z hy hz f hf, _⟩,
id             └──┘        └───────────┘   └──────┘ └┘
src    └─────┘ └──┘   └──┘└───────────┘  └──────┘  └─┘ └─────────────────┘
typ    └─────┘ └──┘  └──┘└───────────┘ └──────┘└┘└─┘ └─────────────────┘
doc    └─────┘ └──┘    └──┘                         └─┘ └─────────────────┘
txt    └─────┘         └──┘                         └─┘ └─────────────────┘
par    └─────┘         └──┘                         └─┘ └─────────────────┘
pid                   └──┘                         └─┘ └─────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
355    have : dist y z < δ := calc
id            └──┘    
src    └─────┘└──┘   └──┘    
typ    └─────┘└──┘└──┘    
doc    └─────┘        └──┘    
txt    └─────┘        └──┘    
par    └─────┘        └──┘    
pid    └───┘└┘        └──┘    
st   ──────────────────────────────
356      dist y z ≤ dist y x + dist z x : dist_triangle_right _ _ _
id                            └──┘     └─────────────────┘
src  ───┘              └──┘  └─┘└─────────────────┘└──────
typ  ───┘             └──┘└─┘└─────────────────┘└──────
doc  ───┘                    └─┘                   └──────
txt  ───┘                    └─┘                   └──────
par  ───┘                    └─┘                   └──────
pid  ───┘                    └─┘                   └──────
st   ───────────────────────────────────────────────────────────────
357      ... < δ/2 + δ/2 : add_lt_add hy hz
id                        └────────┘ └┘ └┘
src  ───────┘   └┘  └──┘└────────┘    
typ  ───────┘   └┘  └──┘└────────┘└┘└┘
doc  ───────┘   └┘   └──┘              
txt  ───────┘   └┘   └──┘              
par  ───────┘   └┘   └──┘              
pid  ───────┘   └┘   └──┘              
st   ───────────────────────────────────────
358      ... = δ : add_halves _,
id                └────────┘
src  ───────┘  └─┘└────────┘└┘
typ  ───────┘ └─┘└────────┘└┘
doc  ───────┘  └─┘          └┘
txt  ───────┘  └─┘          └┘
par  ───────┘  └─┘          └┘
pid  ───────┘  └─┘          └┘
st   ─────────────────────────┘└─
359    calc
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ───────
360      dist (f y) (f z) ≤ b (dist y z) : H y z f hf
id                            └──┘            └┘
src                            └──┘
typ                           └──┘            └┘
st   ─────────────────────────────────────────────────
361      ... ≤ abs (b (dist y z)) : le_abs_self _
id             └─┘                  └─────────┘
src            └─┘                  └─────────┘
typ            └─┘                  └─────────┘
st   ─────────────────────────────────────────────
362      ... = dist (b (dist y z)) 0 : by simp [real.dist_eq]
id                                              └──────────┘
src                                       └────┘└──────────┘└─
typ                                       └────┘└──────────┘└─
doc                                       └────┘            └─
txt                                       └────┘            └─
par                                       └────┘            └─
pid                                                       
st   ───────────────────────────────────┘└────────────────────
363      ... < ε : hδ (by simpa [real.dist_eq] using this),
id                └┘            └──────────┘        └──┘
src  ───┘                 └─────┘└──────────┘└──────┘
typ  ───┘         └┘     └─────┘└──────────┘└──────┘└──┘
doc  ───┘                 └─────┘            └──────┘
txt  ───┘                 └─────┘            └──────┘
par  ───┘                 └─────┘            └──────┘
pid  ───┘                                  └────┘
st   ───┘└──────────────┘└──────────────────────────────┘└─
364  end
st   ──┘
365  
366  end arzela_ascoli
367  
368  section normed_group
369  /- In this section, if β is a normed group, then we show that the space of bounded
370  continuous functions from α to β inherits a normed group structure, by using
371  pointwise operations and checking that they are compatible with the uniform distance. -/
372  
373  variables [topological_space α] [normed_group β]
id              └───────────────┘     └──────────┘
src             └───────────────┘     └──────────┘
typ             └───────────────┘     └──────────┘
doc             └───────────────┘     └──────────┘
374  variables {f g : α →ᵇ β} {x : α} {C : ℝ}
id                      └┘                 
src                     └┘                 
typ                     └┘                 
doc                     └┘
375  
376  instance : has_zero (α →ᵇ β) := ⟨const 0⟩
id              └──────┘   └┘       └───┘
src             └──────┘    └┘        └───┘
typ             └──────┘   └┘       └───┘
doc                         └┘
377  
378  @[simp] lemma coe_zero : (0 : α →ᵇ β) x = 0 := rfl
id                                  └┘          └─┘
src                                  └┘            └─┘
typ                                 └┘          └─┘
doc    └──┘                          └┘
379  
380  instance : has_norm (α →ᵇ β) := ⟨λu, dist u 0⟩
id              └──────┘   └┘          └──┘ 
src             └──────┘    └┘            └──┘
typ             └──────┘   └┘          └──┘ 
doc             └──────┘    └┘
381  
382  lemma norm_def : ∥f∥ = dist f 0 := rfl
id                      └──┘       └─┘
src                      └──┘        └─┘
typ                     └──┘       └─┘
383  
384  lemma norm_coe_le_norm (x : α) : ∥f x∥ ≤ ∥f∥ := calc
id                                      
src                                         
typ                                     
385    ∥f x∥ = dist (f x) ((0 : α →ᵇ β) x) : by simp [dist_zero_right]
id         └──┘            └┘                └─────────────┘
src          └──┘               └┘            └────┘└─────────────┘└─
typ        └──┘            └┘          └────┘└─────────────┘└─
doc                               └┘            └────┘               └─
txt                                             └────┘               └─
par                                             └────┘               └─
pid                                                                
st                                             └───────────────────────
386    ... ≤ ∥f∥ : dist_coe_le_dist _
id              └──────────────┘
src  ─┘          └──────────────┘
typ  ─┘         └──────────────┘
doc  ─┘            └──────────────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
387  
388  /-- Distance between the images of any two points is at most twice the norm of the function. -/
389  lemma dist_le_two_norm (x y : α) : dist (f x) (f y) ≤ 2 * ∥f∥ := calc
id                                     └──┘             
src                                     └──┘                  
typ                                    └──┘             
390    dist (f x) (f y) ≤ ∥f x∥ + ∥f y∥ : dist_le_norm_add_norm _ _
id     └──┘                  └───────────────────┘
src    └──┘                          └───────────────────┘
typ    └──┘                  └───────────────────┘
391                 ... ≤ ∥f∥ + ∥f∥     : add_le_add (norm_coe_le_norm x) (norm_coe_le_norm y)
id                                 └────────┘  └──────────────┘    └──────────────┘ 
src                                  └────────┘  └──────────────┘     └──────────────┘
typ                                └────────┘  └──────────────┘    └──────────────┘ 
392                 ... = 2 * ∥f∥      : (two_mul _).symm
id                                    └─────┘   └──┘
src                                    └─────┘   └──┘
typ                                   └─────┘   └──┘
393  
394  /-- The norm of a function is controlled by the supremum of the pointwise norms -/
395  lemma norm_le (C0 : (0 : ℝ) ≤ C) : ∥f∥ ≤ C ↔ ∀x:α, ∥f x∥ ≤ C :=
id                                               
src                                                   
typ                                              
396  by simpa only [coe_zero, dist_zero_right] using @dist_le _ _ _ _ f 0 _ C0
id                  └──────┘  └─────────────┘         └─────┘              └┘
src     └──────────┘└──────┘└┘└─────────────┘└──────┘ └─────┘└───────┘ └───┘  
typ     └──────────┘└──────┘└┘└─────────────┘└──────┘ └─────┘└───────┘└───┘└┘
doc     └──────────┘        └┘               └──────┘ └─────┘└───────┘ └───┘  
txt     └──────────┘        └┘               └──────┘        └───────┘ └───┘  
par     └──────────┘        └┘               └──────┘        └───────┘ └───┘  
pid          └──┘└┘        └┘               └────┘        └───────┘ └───┘  
st     └───────────────────────────────────────────────────────────────────────
397  
src  
typ  
doc  
txt  
par  
pid  
st   
398  /-- The pointwise sum of two bounded continuous functions is again bounded continuous. -/
399  instance : has_add (α →ᵇ β) :=
id              └─────┘   └┘ 
src             └─────┘    └┘
typ             └─────┘   └┘ 
doc                        └┘
400  ⟨λf g, ⟨λx, f x + g x, f.2.1.add g.2.1,
id                    └─┘   
src                           └─┘    
typ                   └─┘   
401    let ⟨_, fM, hf⟩ := f.2 in let ⟨_, gM, hg⟩ := g.2 in
id     └─┘     └┘  └┘          └─┘     └┘  └┘     
src                                                 
typ    └─┘     └┘  └┘          └─┘     └┘  └┘     
402    ⟨fM + gM, λ x y, dist_add_add_le_of_le (hf _ _) (hg _ _)⟩⟩⟩
id                   └───────────────────┘
src                    └───────────────────┘
typ                  └───────────────────┘
403  
404  /-- The pointwise opposite of a bounded continuous function is again bounded continuous. -/
405  instance : has_neg (α →ᵇ β) :=
id              └─────┘   └┘ 
src             └─────┘    └┘
typ             └─────┘   └┘ 
doc                        └┘
406  ⟨λf, ⟨λx, -f x, f.2.1.neg, by simpa only [dist_neg_neg] using f.2.2⟩⟩
id                └─┘                  └──────────┘        
src                    └─┘      └──────────┘└──────────┘└──────┘ └──┘
typ               └─┘      └──────────┘└──────────┘└──────┘└──┘
doc                                └──────────┘            └──────┘ └──┘
txt                                └──────────┘            └──────┘ └──┘
par                                └──────────┘            └──────┘ └──┘
pid                                     └──┘└┘            └────┘ └┘└┘
st                                └────────────────────────────────────┘
407  
408  @[simp] lemma coe_add : (f + g) x = f x + g x := rfl
id                                          └─┘
src                                                └─┘
typ                                         └─┘
doc    └──┘
409  @[simp] lemma coe_neg : (-f) x = - (f x) := rfl
id                                        └─┘
src                                           └─┘
typ                                       └─┘
doc    └──┘
410  lemma forall_coe_zero_iff_zero : (∀x, f x = 0) ↔ f = 0 :=
id                                                
src                                                   
typ                                               
411  ⟨@ext _ _ _ _ f 0, by rintro rfl _; refl⟩
id     └─┘         
src    └─┘                 └──────────┘  └──┘
typ    └─┘                └──────────┘  └──┘
doc                        └──────────┘  └──┘
txt                        └──────────┘  └──┘
par                        └──────────┘  └──┘
pid                              └────┘
st                        └─────────────────┘
412  
413  instance : add_comm_group (α →ᵇ β) :=
id              └────────────┘   └┘ 
src             └────────────┘    └┘
typ             └────────────┘   └┘ 
doc                               └┘
414  { add_assoc    := assume f g h, by ext; simp,
id                              
src                                     └─┘  └──┘
typ                                  └─┘  └──┘
doc                                     └─┘  └──┘
txt                                     └─┘  └──┘
par                                     └─┘  └──┘
st                                     └────────┘
415    zero_add     := assume f, by ext; simp,
id                            
src                                 └─┘  └──┘
typ                                └─┘  └──┘
doc                                 └─┘  └──┘
txt                                 └─┘  └──┘
par                                 └─┘  └──┘
st                                 └────────┘
416    add_zero     := assume f, by ext; simp,
id                            
src                                 └─┘  └──┘
typ                                └─┘  └──┘
doc                                 └─┘  └──┘
txt                                 └─┘  └──┘
par                                 └─┘  └──┘
st                                 └────────┘
417    add_left_neg := assume f, by ext; simp,
id                            
src                                 └─┘  └──┘
typ                                └─┘  └──┘
doc                                 └─┘  └──┘
txt                                 └─┘  └──┘
par                                 └─┘  └──┘
st                                 └────────┘
418    add_comm     := assume f g, by ext; simp,
id                             
src                                   └─┘  └──┘
typ                                 └─┘  └──┘
doc                                   └─┘  └──┘
txt                                   └─┘  └──┘
par                                   └─┘  └──┘
st                                   └────────┘
419    ..bounded_continuous_function.has_add,
id       └─────────────────────────────────┘
src      └─────────────────────────────────┘
typ      └─────────────────────────────────┘
doc      └─────────────────────────────────┘
420    ..bounded_continuous_function.has_neg,
id       └─────────────────────────────────┘
src      └─────────────────────────────────┘
typ      └─────────────────────────────────┘
doc      └─────────────────────────────────┘
421    ..bounded_continuous_function.has_zero }
id       └──────────────────────────────────┘
src      └──────────────────────────────────┘
typ      └──────────────────────────────────┘
422  
423  @[simp] lemma coe_diff : (f - g) x = f x - g x := rfl
id                                           └─┘
src                                                 └─┘
typ                                          └─┘
doc    └──┘
424  
425  instance : normed_group (α →ᵇ β) :=
id              └──────────┘   └┘ 
src             └──────────┘    └┘
typ             └──────────┘   └┘ 
doc             └──────────┘    └┘
426  normed_group.of_add_dist (λ _, rfl) $ λ f g h,
id   └──────────────────────┘      └─┘        
src  └──────────────────────┘       └─┘
typ  └──────────────────────┘      └─┘        
doc  └──────────────────────┘
427  (dist_le dist_nonneg).2 $ λ x,
id    └─────┘ └─────────┘       
src   └─────┘ └─────────┘ 
typ   └─────┘ └─────────┘       
doc   └─────┘
428  le_trans (by rw [dist_eq_norm, dist_eq_norm, coe_add, coe_add,
id   └──────┘         └──────────┘  └──────────┘  └─────┘  └─────┘
src  └──────┘     └──┘└──────────┘└┘└──────────┘└┘└─────┘└┘└─────┘└─
typ  └──────┘     └──┘└──────────┘└┘└──────────┘└┘└─────┘└┘└─────┘└─
doc               └──┘            └┘            └┘       └┘       └─
txt               └──┘            └┘            └┘       └┘       └─
par               └──┘            └┘            └┘       └┘       └─
pid                 └┘            └┘            └┘       └┘       └─
st               └───────────────┘└────────────┘└───────┘└───────┘└─
429    add_sub_add_right_eq_sub]) (dist_coe_le_dist x)
id     └──────────────────────┘    └──────────────┘ 
src  ─┘└──────────────────────┘   └──────────────┘
typ  ─┘└──────────────────────┘   └──────────────┘ 
doc  ─┘                           └──────────────┘
txt  ─┘                        
par  ─┘                        
pid  ─┘                        
st   ─────────────────────────┘
430  
431  lemma abs_diff_coe_le_dist : norm (f x - g x) ≤ dist f g :=
id                                └──┘         └──┘  
src                               └──┘             └──┘
typ                               └──┘         └──┘  
432  by rw normed_group.dist_eq; exact @norm_coe_le_norm _ _ _ _ (f-g) x
id         └──────────────────┘         └──────────────┘            
src     └─┘└──────────────────┘  └────┘ └──────────────┘└───────┘   └┘ 
typ     └─┘└──────────────────┘  └────┘ └──────────────┘└───────┘ └┘
doc     └─┘                      └────┘                 └───────┘    └┘ 
txt     └─┘                      └────┘                 └───────┘    └┘ 
par     └─┘                      └────┘                 └───────┘    └┘ 
pid                                                   └───────┘    └┘ 
st     └─────────────────────────────────────────────────────────────────
433  
src  
typ  
doc  
txt  
par  
pid  
st   
434  lemma coe_le_coe_add_dist {f g : α →ᵇ ℝ} : f x ≤ g x + dist f g :=
id                                     └┘           └──┘  
src                                     └┘               └──┘
typ                                    └┘           └──┘  
doc                                     └┘
435  sub_le_iff_le_add'.1 $ (abs_le.1 $ @dist_coe_le_dist _ _ _ _ f g x).2
id   └────────────────┘     └────┘     └──────────────┘            
src  └────────────────┘     └────┘     └──────────────┘               
typ  └────────────────┘     └────┘     └──────────────┘            
doc                                      └──────────────┘
436  
437  /-- Constructing a bounded continuous function from a uniformly bounded continuous
438  function taking values in a normed group. -/
439  def of_normed_group {α : Type u} {β : Type v} [topological_space α] [normed_group β]
id                                                  └───────────────┘    └──────────┘ 
src                                                 └───────────────┘     └──────────┘
typ                                                 └───────────────┘    └──────────┘ 
doc                                                 └───────────────┘     └──────────┘
440    (f : α  → β) (C : ℝ) (H : ∀x, norm (f x) ≤ C) (Hf : continuous f) : α →ᵇ β :=
id                               └──┘              └────────┘      └┘ 
src                                 └──┘                 └────────┘        └┘
typ                              └──┘              └────────┘      └┘ 
doc                                                        └────────┘        └┘
441  ⟨λn, f n, ⟨Hf, ⟨C + C, λ m n,
id           └┘          
src                    
typ          └┘          
442    calc dist (f m) (f n) ≤ dist (f m) 0 + dist (f n) 0 : dist_triangle_right _ _ _
id          └──┘           └──┘        └──┘         └─────────────────┘
src         └──┘               └──┘          └──┘           └─────────────────┘
typ         └──┘           └──┘        └──┘         └─────────────────┘
443         ... = norm (f m) + norm (f n) : by simp
id                └──┘      └──┘   
src               └──┘        └──┘            └────
typ               └──┘      └──┘          └────
doc                                            └────
txt                                            └────
par                                            └────
pid                                                
st                                            └─────
444         ... ≤ C + C : add_le_add (H m) (H n)⟩⟩⟩
id                     └────────┘       
src  ──────┘             └────────┘
typ  ──────┘           └────────┘       
doc  ──────┘
txt  ──────┘
par  ──────┘
pid  ──────┘
st   ──────┘
445  
446  /-- Constructing a bounded continuous function from a uniformly bounded
447  function on a discrete space, taking values in a normed group -/
448  def of_normed_group_discrete {α : Type u} {β : Type v}
449    [topological_space α] [discrete_topology α] [normed_group β]
id      └───────────────┘    └───────────────┘    └──────────┘ 
src     └───────────────┘     └───────────────┘     └──────────┘
typ     └───────────────┘    └───────────────┘    └──────────┘ 
doc     └───────────────┘     └───────────────┘     └──────────┘
450    (f : α  → β) (C : ℝ) (H : ∀x, norm (f x) ≤ C) : α →ᵇ β :=
id                               └──┘           └┘ 
src                                 └──┘               └┘
typ                              └──┘           └┘ 
doc                                                      └┘
451  of_normed_group f C H continuous_of_discrete_topology
id   └─────────────┘    └─────────────────────────────┘
src  └─────────────┘       └─────────────────────────────┘
typ  └─────────────┘    └─────────────────────────────┘
doc  └─────────────┘
452  
453  end normed_group
454  end bounded_continuous_function